T:Type, t:T, l:IdLnk, ds1, ds2:x:Id fp Type, P:(State(ds1)), Q:(State(ds2)),
d1:(s:State(ds1). Dec(n:. (((P(s,n)))))), d2:(s:State(ds2). Dec(n:. (((Q(s,n)))))),
f:(State(ds1)T).
Normal(ds1)
 Normal(ds2)
 ((destination(l) = source(l)  Id))
 (sendMinimalR{a:ut2, tg:ut2}(T; t; l; ds1; ds2; P; Q; d1; d2; f)  Realizer) 

latex

Definitions	t  T, Type, x:A  B(x), IdLnk, a:A fp B(a), x:AB(x), b, A, Dec(P), xdom(f). v=f(x)   P(x;v), Normal(ds), False, x:A. B(x), , weakSendDoApplyR{$a:ut2, $tg:ut2}(T; t; l; ds; f), [], [car / cdr], sendMinimalR{$a:ut2, $tg:ut2}(T; t; l; ds1; ds2; P; Q; d1; d2; f), a = b, P  Q, P  Q, Id, s = t, P & Q, P  Q, Realizer, State(ds), x:A. B(x),
Lemmas	not functionality wrt iff, assert-eq-id, Rlist wf